<html>
<head><meta charset="utf-8"><title>is symbolic execution worth implementing? · general · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/index.html">general</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html">is symbolic execution worth implementing?</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="204148771"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204148771" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alex <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204148771">(Jul 16 2020 at 21:58)</a>:</h4>
<p>Hey Rustaceans,<br>
I'm new to Rust, so, probably, I'm missing something.<br>
I cannot figure out the status of the issue <a href="https://github.com/rust-lang/miri/issues/440">https://github.com/rust-lang/miri/issues/440</a></p>
<p>The issue is not resolved yet, but no active work has been done for quite a while.<br>
Also, in the issue SEER (Symbolic execution tool) is mentioned, but it looks unfinished. <br>
So, I wonder why is that?</p>
<p>Has the Rust community shifted their attention towards other more important issues?<br>
Or the amount of effort it requires is not reasonable to get little benefits?</p>
<p>Can someone comment on the this?</p>



<a name="204149474"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204149474" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jonas Schievink  [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204149474">(Jul 16 2020 at 22:06)</a>:</h4>
<p>I don't think symbolic execution was ever really in the focus of the Rust community, let alone the Rust team.</p>



<a name="204149510"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204149510" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jonas Schievink  [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204149510">(Jul 16 2020 at 22:07)</a>:</h4>
<p>(as in, there was never a community group focused on working on symbolic execution)</p>



<a name="204149608"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204149608" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jonas Schievink  [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204149608">(Jul 16 2020 at 22:08)</a>:</h4>
<p>There's also MIRAI (<a href="https://github.com/facebookexperimental/MIRAI">https://github.com/facebookexperimental/MIRAI</a>), which does abstract interpretation and is actively developed. Not sure what the difference between that and symbolic execution are though.</p>



<a name="204149675"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204149675" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204149675">(Jul 16 2020 at 22:09)</a>:</h4>
<p><a href="https://github.com/facebookexperimental/MIRAI/blob/master/documentation/Overview.md#verification-is-not-on-the-table">https://github.com/facebookexperimental/MIRAI/blob/master/documentation/Overview.md#verification-is-not-on-the-table</a></p>



<a name="204149684"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204149684" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204149684">(Jul 16 2020 at 22:09)</a>:</h4>
<p>looks like they only want to do a subset of what's possible with symbolic execution</p>



<a name="204149902"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204149902" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204149902">(Jul 16 2020 at 22:12)</a>:</h4>
<p>btw at one point I tried to get klee working with #[no_std] crates but it crashed :( <a href="https://github.com/klee/klee/issues/1263">https://github.com/klee/klee/issues/1263</a></p>



<a name="204150024"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204150024" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jonas Schievink  [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204150024">(Jul 16 2020 at 22:13)</a>:</h4>
<p>It's not entirely unlikely that we'll be working on verification tooling (model checking, etc.) as part of Sealed Rust, but that's probably still many years off</p>



<a name="204153796"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204153796" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alex <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204153796">(Jul 16 2020 at 23:02)</a>:</h4>
<p>That makes sense for me. Thanks!<br>
I will look closer at MIRAI and monitor the issue in KLEE.</p>



<a name="204153890"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204153890" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204153890">(Jul 16 2020 at 23:04)</a>:</h4>
<p>FWIW the KLEE issue is not specific to rust, it's just a general unimplemented feature that happens not to show up much in C</p>



<a name="204154415"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204154415" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204154415">(Jul 16 2020 at 23:12)</a>:</h4>
<p>there's also <a href="https://github.com/PLSysSec/haybale/">https://github.com/PLSysSec/haybale/</a></p>



<a name="204640663"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204640663" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> eddyb <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204640663">(Jul 22 2020 at 08:24)</a>:</h4>
<p>cc <span class="user-mention" data-user-id="124288">@oli</span> (I think there was someone else working on symbolic execution, and it was based on miri itself)</p>



<a name="204640700"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204640700" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204640700">(Jul 22 2020 at 08:24)</a>:</h4>
<p>cc <span class="user-mention" data-user-id="132916">@Christian Poveda</span></p>



<a name="204640766"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204640766" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> eddyb <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204640766">(Jul 22 2020 at 08:25)</a>:</h4>
<p>(sadly Zulip doesn't give me a full completion list, at least I did try <code>@C</code>)</p>



<a name="204640842"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204640842" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204640842">(Jul 22 2020 at 08:26)</a>:</h4>
<p>I'd like to have symbolic execution support in the miri engine, but I don't have a clear picture of how to do this without affecting CTFE performance and complexity yet</p>



<a name="204640874"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204640874" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204640874">(Jul 22 2020 at 08:26)</a>:</h4>
<p>I still believe it's possible, but that's mainly a model I have in my head and have never written down</p>



<a name="204657418"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204657418" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204657418">(Jul 22 2020 at 12:14)</a>:</h4>
<p><span class="user-mention" data-user-id="308841">@Alex</span>, we've been using <a href="https://github.com/christianpoveda/sire">sire</a> to do const-generics "unification" however the whole project is just a proof of concept</p>



<a name="204657674"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204657674" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204657674">(Jul 22 2020 at 12:17)</a>:</h4>
<p>in particular, we cannot execute every possible Rust program yet, some stuff like loops or adts are just things that we've haven't implemented yet, other things like pointers I haven't thought how to handle that correctly</p>



<a name="204657708"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204657708" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204657708">(Jul 22 2020 at 12:17)</a>:</h4>
<p>the other problem is that we need an SMT solver to do symbolic execution, we could probably move away from it but we aren't there yet.</p>



<a name="204657793"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204657793" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204657793">(Jul 22 2020 at 12:18)</a>:</h4>
<p>I think symbolic execution benefits are great but we'd have to come up with a design that feels like an integral part of the compiler</p>



<a name="204658861"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204658861" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204658861">(Jul 22 2020 at 12:31)</a>:</h4>
<p>and also most of the things we win with it feel like nice-to-haves rather than critical features</p>



<a name="204658971"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204658971" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204658971">(Jul 22 2020 at 12:32)</a>:</h4>
<p>maybe when const generics get stabilized, it will make symbolic execution more relevant but maybe there are better ways to solve unification.</p>



<a name="204874226"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204874226" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alex <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204874226">(Jul 24 2020 at 02:40)</a>:</h4>
<p>Did I get it right that const-generics "unification" can be further explored with sire? if it is the case I would be happy to implement new features or stabilize the existing ones as well as explore uncertain questions. <br>
I find sire interesting to work on.</p>
<p>Are there any reasons that block further development of sire?</p>
<p>And if it's ok for me to work on the project, where is the best place to start? <span class="user-mention" data-user-id="132916">@Christian Poveda</span></p>



<a name="204874761"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204874761" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204874761">(Jul 24 2020 at 02:55)</a>:</h4>
<p>Even though sire has a lot of room for improvement I wouldn't invest more effort in it right now, the project itself was more a proof of concept to see if it was possible to use symbolic execution to unify constants, and the answer is  "yes you can".</p>
<p>The parts that need more work as <span class="user-mention" data-user-id="124288">@oli</span> said is figuring out how to fit something like sire inside the compiler without compromising the performance of the constant evaluation engine. And to be honest I think nobody has any idea about how should we tackle that.</p>



<a name="204874957"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204874957" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204874957">(Jul 24 2020 at 03:01)</a>:</h4>
<p>I hope my answer isn't too discouraging. I think the big blocker here is that we haven't been able to answer the same question you asked in this topic: "is it even worth it to implement symbolic execution?". </p>
<p>It can be used for constant unification, and that's cool but that doesn't mean is the only solution (it isn't the first either: <a href="https://github.com/rust-lang/rfcs/issues/1930">https://github.com/rust-lang/rfcs/issues/1930</a>)</p>



<a name="204887344"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204887344" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204887344">(Jul 24 2020 at 07:43)</a>:</h4>
<p>let's add "and without compromising the readability/maintainability of the CTFE engine" to the list; personally I am even more worried about that than performance</p>



<a name="204926157"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/is%20symbolic%20execution%20worth%20implementing%3F/near/204926157" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/is.20symbolic.20execution.20worth.20implementing.3F.html#204926157">(Jul 24 2020 at 14:58)</a>:</h4>
<p>yeah completely</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>